Prop-NoDisjointConstructors.agda:10,1-9
_ ≡Prop _ should be empty, but the following constructor patterns
are valid:
  refl
when checking the clause left hand side
p₁≢p₂ ()
